@madvorak can you please do at least one of the following?

1. link to a Zulip thread discussing these changes
2. provide an explain of the benefits gained on the types ℝ≥0, ℕ or ℚ≥0 by having this class (as opposed to having the pieces of it separately, which we already have)
3. other examples of types satisfying this class, and what is gained by having it (e.g., what new useful theorems can you prove that you can't with existing classes?)

@madvorak can you please do at least one of the following?

1. link to a Zulip thread discussing these changes
2. provide an explain of the benefits gained on the types ℝ≥0, ℕ or ℚ≥0 by having this class (as opposed to having the pieces of it separately, which we already have)
3. other examples of types satisfying this class, and what is gained by having it (e.g., what new useful theorems can you prove that you can't with existing classes?)

I added the link to the Zulip thread, even tho there isn't much.

Other examples are tuples:

instance : CanonicallyOrderedAddCancelCommMonoid (NNReal × NNRat × Nat) := inferInstance

Is like CanonicallyOrderedAddCancelCommMonoid as it essentially is only two symbols but a lot of structure (one of the strongest classes without LinearOrder that you can have).

@madvorak thanks, but the thread you link to doesn't provide any context about why you want this class.

Is there some theorem you want to generalize or what? Adding useful type classes is fine, but adding them just for the sake of filling out all possible nodes of the hierarchy is something we want to avoid.

I'm not accusing you of the latter, I would just like documented somewhere the reason we have this class.

Sorry, I do not have time to review this before two months at least.